(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.add ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.multiply ($$unsorted $$unsorted) $$unsorted)
(assert (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (= (tptp.multiply X (tptp.add Y Z)) (tptp.add (tptp.multiply Y X) (tptp.multiply Z X)))))
(declare-fun tptp.inverse ($$unsorted) $$unsorted)
(declare-fun tptp.one () $$unsorted)
(assert (forall ((X $$unsorted)) (= (tptp.add X (tptp.inverse X)) tptp.one)))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (let ((_let_1 (tptp.inverse X))) (= (tptp.add (tptp.multiply X _let_1) (tptp.add (tptp.multiply X Y) (tptp.multiply _let_1 Y))) Y))))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (let ((_let_1 (tptp.inverse Y))) (= (tptp.add (tptp.multiply X _let_1) (tptp.add (tptp.multiply X Y) (tptp.multiply _let_1 Y))) X))))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (let ((_let_1 (tptp.inverse Y))) (= (tptp.add (tptp.multiply X _let_1) (tptp.add (tptp.multiply X X) (tptp.multiply _let_1 X))) X))))
(declare-fun tptp.a () $$unsorted)
(assert (not (= (tptp.add tptp.a tptp.a) tptp.a)))
(set-info :filename BOO027-1)
(check-sat)
